\MySection{Example Boolean Function}\label{GenePoolBool}
\noindent
Context:
\begin{verbatim}
/*--------------------------------------*/
true = Lam X . lam x : X . lam y : X . x;
false = Lam X . lam x : X . lam y : X . y;
TyBool = TT X . X -> X ->X;
/**********************************************/
\end{verbatim}
\noindent
\noindent
The following gene pool was created randomly using the context defined above. It contains 70 elements and has a total complexity
of 2923 units. The generation procedure was instructed to refuse any gene with complexity greater than 85 units.
{\tiny
\begin{verbatim}
type: (TyBool)-> (TT E. ((TyBool)-> E)-> E)
   id:0  lam h:TyBool.Lam R.lam r:(TyBool)-> R.r h
type: (TyBool)-> ((TyBool)-> (TT W. (((TyBool)-> (TyBool))-> W)-> W))-> ((TyBool)-> (TT R. (((TyBool)-> (TyBool))-> R)-> R))-> (TyBool)-> (TT U. (((TyBool)-> (TyBool))-> U)-> U)
   id:0  lam g:TyBool.g [(TyBool)-> (TT W. (((TyBool)-> (TyBool))-> W)-> W)]
type: (TyBool)-> ((TyBool)-> (TT M. ((TyBool)-> M)-> M))-> ((TyBool)-> (TT T. ((TyBool)-> T)-> T))-> (TyBool)-> (TT M. ((TyBool)-> M)-> M)
   id:0  lam q:TyBool.q [(TyBool)-> (TT R. ((TyBool)-> R)-> R)]
type: (TyBool)-> (TyBool)-> ((TyBool)-> ((TyBool)-> (TyBool))-> ((TyBool)-> (TyBool))-> (TyBool)-> (TyBool))-> ((TyBool)-> ((TyBool)-> (TyBool))-> ((TyBool)-> (TyBool))-> (TyBool)-> (TyBool))-> (TyBool)-> ((TyBool)-> (TyBool))-> ((TyBool)-> (TyBool))-> (TyBool)-> (TyBool)
   id:0  lam g:TyBool.lam r:TyBool.r [(TyBool)-> ((TyBool)-> (TyBool))-> ((TyBool)-> (TyBool))-> (TyBool)-> (TyBool)]
type: (((TyBool)-> (TyBool))-> (TyBool)-> (TT F. (((TyBool)-> (TyBool))-> F)-> F))-> (TyBool)-> (TT W. (((TyBool)-> (TyBool))-> W)-> W)
   id:1  lam r:((TyBool)-> (TyBool))-> (TyBool)-> (TT F. (((TyBool)-> (TyBool))-> F)-> F).r (lam q:TyBool.false)
   id:0  lam p:((TyBool)-> (TyBool))-> (TyBool)-> (TT V. (((TyBool)-> (TyBool))-> V)-> V).p (lam r:TyBool.true)
type: ((TyBool)-> (TT A. (((TyBool)-> (TyBool))-> A)-> A))-> (TyBool)-> (TT Q. (((TyBool)-> (TyBool))-> Q)-> Q)
   id:0  lam n:(TyBool)-> (TT S. (((TyBool)-> (TyBool))-> S)-> S).n
type: (TyBool)-> ((TyBool)-> (TyBool)-> (TT I. (((TyBool)-> (TyBool))-> I)-> I))-> (TyBool)-> (TT O. (((TyBool)-> (TyBool))-> O)-> O)
   id:0  lam l:TyBool.lam y:(TyBool)-> (TyBool)-> (TT V. (((TyBool)-> (TyBool))-> V)-> V).y l
type: (TyBool)-> (((TyBool)-> (TyBool))-> (TyBool)-> (TT Y. (((TyBool)-> (TyBool))-> Y)-> Y))-> (TyBool)-> (TT I. (((TyBool)-> (TyBool))-> I)-> I)
   id:0  lam e:TyBool.lam l:((TyBool)-> (TyBool))-> (TyBool)-> (TT H. (((TyBool)-> (TyBool))-> H)-> H).l (lam w:TyBool.e)
type: ((TyBool)-> (TT M. (((TyBool)-> (TyBool))-> M)-> M))-> ((TyBool)-> (TT W. (((TyBool)-> (TyBool))-> W)-> W))-> (TyBool)-> (TT Y. (((TyBool)-> (TyBool))-> Y)-> Y)
   id:0  lam x:(TyBool)-> (TT P. (((TyBool)-> (TyBool))-> P)-> P).lam h:(TyBool)-> (TT L. (((TyBool)-> (TyBool))-> L)-> L).h
type: (TyBool)-> ((TyBool)-> (TyBool)-> (TT R. ((TyBool)-> R)-> R))-> (TyBool)-> (TT Q. ((TyBool)-> Q)-> Q)
   id:0  lam g:TyBool.lam w:(TyBool)-> (TyBool)-> (TT A. ((TyBool)-> A)-> A).w g
type: (TyBool)-> (((TyBool)-> (TyBool))-> (TyBool)-> (TT E. ((TyBool)-> E)-> E))-> (TyBool)-> (TT D. ((TyBool)-> D)-> D)
   id:0  lam s:TyBool.lam u:((TyBool)-> (TyBool))-> (TyBool)-> (TT I. ((TyBool)-> I)-> I).u (lam v:TyBool.s)
type: (TyBool)-> (TT G. (((TyBool)-> (TyBool))-> G)-> G)
   id:0  lam k:TyBool.Lam J.lam b:((TyBool)-> (TyBool))-> J.b (lam j:TyBool.k)
type: (((TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)-> (TyBool)
   id:1  lam f:((TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)-> (TyBool).f (lam s:TyBool.false)
   id:0  lam v:((TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)-> (TyBool).v (lam s:TyBool.true)
type: (TyBool)-> (TyBool)-> (TyBool)-> (TyBool)-> (TyBool)
   id:0  lam r:TyBool.lam d:TyBool.d [TyBool]
type: (TyBool)-> ((TyBool)-> (TyBool)-> (((TyBool)-> (TyBool))-> (TyBool))-> (TyBool))-> (TyBool)-> (((TyBool)-> (TyBool))-> (TyBool))-> (TyBool)
   id:0  lam o:TyBool.lam o':(TyBool)-> (TyBool)-> (((TyBool)-> (TyBool))-> (TyBool))-> (TyBool).o' o
type: (TyBool)-> ((TyBool)-> (TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)
   id:0  lam r:TyBool.lam u:(TyBool)-> (TyBool)-> (TyBool)-> (TyBool).u r
type: (TyBool)-> (((TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)
   id:0  lam s:TyBool.lam q:((TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool).q (lam x:TyBool.s)
type: (TyBool)-> ((TyBool)-> (TyBool))-> ((TyBool)-> (TyBool))-> (TyBool)-> (TyBool)
   id:0  lam q:TyBool.q [(TyBool)-> (TyBool)]
type: ((TyBool)-> (TyBool)-> (TyBool))-> ((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)
   id:0  lam f:(TyBool)-> (TyBool)-> (TyBool).lam i:(TyBool)-> (TyBool)-> (TyBool).i
type: (TyBool)-> ((TyBool)-> (TyBool))-> (TyBool)
   id:0  lam n:TyBool.lam x:(TyBool)-> (TyBool).x n
type: (TyBool)-> (((TyBool)-> (TyBool))-> (TyBool))-> (TyBool)
   id:0  lam x:TyBool.lam o:((TyBool)-> (TyBool))-> (TyBool).o (lam w:TyBool.x)
type: (TyBool)-> (TyBool)-> (TyBool)
   id:1  lam s:TyBool.lam c:TyBool.c
   id:0  lam h:TyBool.lam u:TyBool.h
type: (TyBool)-> (TyBool)-> ((TyBool)-> ((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool))-> ((TyBool)-> ((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool))-> (TyBool)-> ((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)
   id:0  lam f:TyBool.lam p:TyBool.p [(TyBool)-> ((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)]
type: (TyBool)-> (TyBool)-> ((TyBool)-> (((TyBool)-> (TyBool))-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool))-> ((TyBool)-> (((TyBool)-> (TyBool))-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool))-> (TyBool)-> (((TyBool)-> (TyBool))-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)
   id:0  lam j:TyBool.lam n:TyBool.n [(TyBool)-> (((TyBool)-> (TyBool))-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)]
type: (TyBool)-> (TyBool)-> ((TyBool)-> (TyBool)-> (TyBool)-> (TyBool))-> ((TyBool)-> (TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)-> (TyBool)
   id:0  lam m:TyBool.lam h:TyBool.h [(TyBool)-> (TyBool)-> (TyBool)-> (TyBool)]
type: (TyBool)-> (TyBool)-> (((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool))-> (((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool))-> ((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)
   id:0  lam n:TyBool.lam s:TyBool.s [((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)]
type: (TyBool)-> (TyBool)-> ((TyBool)-> (TyBool))-> ((TyBool)-> (TyBool))-> (TyBool)-> (TyBool)
   id:0  lam t:TyBool.lam f:TyBool.f [(TyBool)-> (TyBool)]
type: (TyBool)-> ((TyBool)-> (TyBool)-> (((TyBool)-> (TyBool))-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool))-> (TyBool)-> (((TyBool)-> (TyBool))-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)
   id:0  lam p:TyBool.lam k:(TyBool)-> (TyBool)-> (((TyBool)-> (TyBool))-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool).k p
type: (TyBool)-> ((TyBool)-> (TyBool)-> (TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)-> (TyBool)
   id:0  lam b:TyBool.lam e:(TyBool)-> (TyBool)-> (TyBool)-> (TyBool)-> (TyBool).e b
type: (TyBool)-> ((TyBool)-> ((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool))-> ((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)
   id:0  lam i:TyBool.lam m:(TyBool)-> ((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool).m i
type: (TyBool)-> (((TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)-> (TyBool)
   id:0  lam y:TyBool.lam n:((TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)-> (TyBool).n (lam y':TyBool.y)
type: (TyBool)-> ((TyBool)-> (TyBool)-> (TyBool))-> ((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)
   id:0  lam u:TyBool.u [(TyBool)-> (TyBool)-> (TyBool)]
type: (TyBool)-> (TyBool)
   id:0  lam j:TyBool.j
type: (TyBool)-> (TyBool)-> ((TyBool)-> (TT T. ((TyBool)-> T)-> T))-> ((TyBool)-> (TT J. ((TyBool)-> J)-> J))-> (TyBool)-> (TT C. ((TyBool)-> C)-> C)
   id:0  lam g:TyBool.lam v:TyBool.v [(TyBool)-> (TT I. ((TyBool)-> I)-> I)]
type: (TyBool)-> (TyBool)-> ((TyBool)-> (TT R. (((TyBool)-> (TyBool))-> R)-> R))-> ((TyBool)-> (TT D. (((TyBool)-> (TyBool))-> D)-> D))-> (TyBool)-> (TT D. (((TyBool)-> (TyBool))-> D)-> D)
   id:0  lam b:TyBool.lam x:TyBool.x [(TyBool)-> (TT M. (((TyBool)-> (TyBool))-> M)-> M)]
type: (TyBool)-> (TyBool)-> ((TyBool)-> ((TyBool)-> (TyBool))-> (TyBool))-> ((TyBool)-> ((TyBool)-> (TyBool))-> (TyBool))-> (TyBool)-> ((TyBool)-> (TyBool))-> (TyBool)
   id:0  lam d:TyBool.lam g:TyBool.g [(TyBool)-> ((TyBool)-> (TyBool))-> (TyBool)]
type: (TyBool)-> (TyBool)-> ((TyBool)-> (((TyBool)-> (TyBool))-> (TyBool))-> (TyBool))-> ((TyBool)-> (((TyBool)-> (TyBool))-> (TyBool))-> (TyBool))-> (TyBool)-> (((TyBool)-> (TyBool))-> (TyBool))-> (TyBool)
   id:0  lam q:TyBool.lam w:TyBool.w [(TyBool)-> (((TyBool)-> (TyBool))-> (TyBool))-> (TyBool)]
type: (TyBool)-> (TyBool)-> ((TyBool)-> (TyBool)-> (TyBool))-> ((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)
   id:0  lam c:TyBool.lam k:TyBool.k [(TyBool)-> (TyBool)-> (TyBool)]
type: (TyBool)-> ((TyBool)-> (TyBool)-> ((TyBool)-> (TyBool))-> ((TyBool)-> (TyBool))-> (TyBool)-> (TyBool))-> (TyBool)-> ((TyBool)-> (TyBool))-> ((TyBool)-> (TyBool))-> (TyBool)-> (TyBool)
   id:0  lam o:TyBool.lam y:(TyBool)-> (TyBool)-> ((TyBool)-> (TyBool))-> ((TyBool)-> (TyBool))-> (TyBool)-> (TyBool).y o
type: (TyBool)-> (((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool))-> (((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool))-> ((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)
   id:0  lam g:TyBool.g [((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)]
type: ((TyBool)-> (TyBool)-> (((TyBool)-> (TyBool))-> (TyBool))-> (TyBool))-> (TyBool)-> (((TyBool)-> (TyBool))-> (TyBool))-> (TyBool)
   id:1  lam j:(TyBool)-> (TyBool)-> (((TyBool)-> (TyBool))-> (TyBool))-> (TyBool).j (false)
   id:0  lam r:(TyBool)-> (TyBool)-> (((TyBool)-> (TyBool))-> (TyBool))-> (TyBool).r (true)
type: (TyBool)-> ((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)
   id:0  lam k:TyBool.lam r:(TyBool)-> (TyBool)-> (TyBool).r k
type: (TyBool)-> (((TyBool)-> (TyBool))-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)
   id:0  lam b:TyBool.lam w:((TyBool)-> (TyBool))-> (TyBool)-> (TyBool).w (lam l:TyBool.b)
type: (TyBool)-> (TyBool)-> (TyBool)-> (TyBool)
   id:0  lam n:TyBool.n [TyBool]
type: ((TyBool)-> (TyBool)-> (TyBool))-> (TyBool)-> (TyBool)-> (TyBool)
   id:0  lam r:(TyBool)-> (TyBool)-> (TyBool).r
type: TyBool
   id:1  true
   id:0  false

\end{verbatim}
}

\MySection{Example 1}\label{genepoolex1}
\noindent
Context:
\begin{verbatim}
/*--------------------------------------*/
gt : Int -> Int -> (TT X . X -> X -> X);
plus : Int -> Int -> Int;
minus : Int -> Int -> Int;
times : Int -> Int -> Int;
div : Int -> Int -> Int;
time : Int;
zero : Int;
one : Int;
/**********************************************/
\end{verbatim}
\noindent
The following gene pool was created randomly using the context defined above. It contains 138 elements and has a total complexity
of 1135 units. The generation procedure was instructed to refuse any gene with complexity greater than 55 units.
{\tiny
\begin{verbatim}
type: Int-> ((Int-> Int)-> Int-> (TT Q. (Int-> Q)-> Q))-> Int-> (TT O. (Int-> O)-> O)
   id:0  lam o:Int.lam h:(Int-> Int)-> Int-> (TT H. (Int-> H)-> H).h (plus o)
type: Int
   id:34  plus time 0
   id:33  minus 0 0
   id:32  minus 1 0
   id:31  minus time 0
   id:30  plus (div time 1) 0
   id:29  plus (div time 0) 0
   id:28  plus (div time time) 0
   id:27  div (div time time) 0
   id:26  times (div time time) 0
   id:25  minus (div time time) 0
   id:24  div 1 0
   id:23  div (div time 1) 0
   id:22  times (div time 1) 0
   id:21  minus (div time 1) 0
   id:20  times 1 0
   id:19  div 0 0
   id:18  minus (times time 1) 0
   id:17  minus (times time 0) 0
   id:16  minus (times time time) 0
   id:15  minus (times time (div time time)) 0
   id:14  minus (times time (div time 0)) 0
   id:13  minus (times time (div time 1)) 0
   id:12  minus (div time 0) 0
   id:11  times time 1
   id:10  times time 0
   id:9  times time time
   id:8  times time (div time time)
   id:7  times time (div time 0)
   id:6  times time (div time 1)
   id:5  div time 1
   id:4  div time 0
   id:3  div time time
   id:2  time
   id:1  zero
   id:0  one
type: Int-> (TT P. ((TT I. I-> I-> I)-> P)-> P)
   id:0  lam e:Int.Lam C.lam l:(TT F. F-> F-> F)-> C.l (gt 0 e)
type: Int-> (TT W. W-> W-> W)
   id:3  lam l:Int.gt 0 l
   id:2  gt 1
   id:1  gt 0
   id:0  gt time
type: Int-> ((Int-> Int)-> Int-> (TT X. ((Int-> Int)-> X)-> X))-> Int-> (TT B. ((Int-> Int)-> B)-> B)
   id:0  lam r:Int.lam h:(Int-> Int)-> Int-> (TT M. ((Int-> Int)-> M)-> M).h (plus r)
type: Int-> ((Int-> Int)-> Int-> (TT R. ((TT W. W-> W-> W)-> R)-> R))-> Int-> (TT L. ((TT T. T-> T-> T)-> L)-> L)
   id:0  lam n:Int.lam s:(Int-> Int)-> Int-> (TT H. ((TT R. R-> R-> R)-> H)-> H).s (plus n)
type: Int-> Int-> Int
   id:7  lam g:Int.plus g
   id:6  lam g:Int.div g
   id:5  lam e:Int.times e
   id:4  lam q:Int.minus q
   id:3  plus
   id:2  minus
   id:1  times
   id:0  div
type: Int-> ((Int-> Int)-> Int-> Int-> Int)-> Int-> Int-> Int
   id:0  lam b:Int.lam d:(Int-> Int)-> Int-> Int-> Int.d (plus b)
type: Int-> ((Int-> Int)-> Int-> Int-> (TT J. J-> J-> J))-> Int-> Int-> (TT L. L-> L-> L)
   id:0  lam f:Int.lam p:(Int-> Int)-> Int-> Int-> (TT O. O-> O-> O).p (plus f)
type: Int-> Int
   id:58  plus (times time (div time 1))
   id:57  plus (times time (div time 0))
   id:56  plus (times time (div time time))
   id:55  plus (times time time)
   id:54  plus (times time 0)
   id:53  plus (times time 1)
   id:52  plus (minus (div time 0) 0)
   id:51  plus (minus (times time (div time 1)) 0)
   id:50  plus (minus (times time (div time 0)) 0)
   id:49  plus (minus (times time (div time time)) 0)
   id:48  plus (minus (times time time) 0)
   id:47  plus (minus (times time 0) 0)
   id:46  plus (minus (times time 1) 0)
   id:45  plus (div 0 0)
   id:44  plus (times 1 0)
   id:43  plus (minus (div time 1) 0)
   id:42  plus (times (div time 1) 0)
   id:41  plus (div (div time 1) 0)
   id:40  plus (div 1 0)
   id:39  plus (minus (div time time) 0)
   id:38  plus (times (div time time) 0)
   id:37  plus (div (div time time) 0)
   id:36  plus (plus (div time time) 0)
   id:35  plus (plus (div time 0) 0)
   id:34  plus (plus (div time 1) 0)
   id:33  plus (minus time 0)
   id:32  plus (minus 1 0)
   id:31  plus (minus 0 0)
   id:30  plus (plus time 0)
   id:29  minus (div time 0)
   id:28  minus (times time (div time 1))
   id:27  minus (times time (div time 0))
   id:26  minus (times time (div time time))
   id:25  minus (times time time)
   id:24  minus (times time 0)
   id:23  minus (times time 1)
   id:22  lam b:Int.div 0 b
   id:21  times 1
   id:20  minus (div time 1)
   id:19  times (div time 1)
   id:18  div (div time 1)
   id:17  lam b:Int.div 1 b
   id:16  minus (div time time)
   id:15  times (div time time)
   id:14  div (div time time)
   id:13  plus (div time time)
   id:12  plus (div time 0)
   id:11  plus (div time 1)
   id:10  lam e:Int.minus time e
   id:9  times time
   id:8  minus 1
   id:7  minus 0
   id:6  minus time
   id:5  plus 1
   id:4  plus 0
   id:3  plus time
   id:2  div 1
   id:1  div 0
   id:0  div time
type: Int-> ((Int-> Int)-> (TT K. K-> K-> K))-> (TT I. I-> I-> I)
   id:0  lam p:Int.lam f:(Int-> Int)-> (TT K. K-> K-> K).f (plus p)
type: Int-> Int-> (TT O. O-> O-> O)
   id:0  gt
type: Int-> (TT R. ((Int-> Int)-> R)-> R)
   id:2  lam b:Int.Lam D.lam d:(Int-> Int)-> D.d (plus b)
   id:1  lam n:Int.Lam T.lam q:(Int-> Int)-> T.q (times n)
   id:0  lam f:Int.Lam E.lam w:(Int-> Int)-> E.w (minus f)
type: Int-> ((Int-> Int)-> Int)-> Int
   id:0  lam j:Int.lam v:(Int-> Int)-> Int.v (plus j)
type: Int-> ((Int-> Int)-> Int-> Int)-> Int-> Int
   id:0  lam n:Int.lam l:(Int-> Int)-> Int-> Int.l (plus n)
type: Int-> (TT H. (Int-> H)-> H)
   id:2  lam j:Int.Lam I.lam o:Int-> I.o (div 0 j)
   id:1  lam u:Int.Lam K.lam m:Int-> K.m (div 1 u)
   id:0  lam b:Int.Lam D.lam a:Int-> D.a (minus time b)
type: Int-> ((Int-> Int)-> Int-> (TT P. P-> P-> P))-> Int-> (TT V. V-> V-> V)
   id:0  lam w:Int.lam c:(Int-> Int)-> Int-> (TT A. A-> A-> A).c (plus w)
type: TT D. D-> D-> D
   id:14  gt 0 1
   id:13  gt 0 0
   id:12  gt 0 time
   id:11  gt 0 (div time time)
   id:10  gt 0 (div time 0)
   id:9  gt 0 (div time 1)
   id:8  gt 1 1
   id:7  gt 1 0
   id:6  gt 1 time
   id:5  gt 1 (div time time)
   id:4  gt 1 (div time 0)
   id:3  gt 1 (div time 1)
   id:2  gt time 1
   id:1  gt time 0
   id:0  gt time time

\end{verbatim}
}
